0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 87 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 26 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
len1B_in_ga([], 0) → len1B_out_ga([], 0)
len1B_in_ga(.(T6, []), s(0)) → len1B_out_ga(.(T6, []), s(0))
len1B_in_ga(.(T6, .(T17, T18)), T9) → U3_ga(T6, T17, T18, T9, len1A_in_ga(T18, X27))
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T24, T25), X42) → U1_ga(T24, T25, X42, len1A_in_ga(T25, X41))
len1A_in_ga(.(T24, T25), s(T29)) → U2_ga(T24, T25, T29, len1A_in_ga(T25, T29))
U2_ga(T24, T25, T29, len1A_out_ga(T25, T29)) → len1A_out_ga(.(T24, T25), s(T29))
U1_ga(T24, T25, X42, len1A_out_ga(T25, X41)) → len1A_out_ga(.(T24, T25), X42)
U3_ga(T6, T17, T18, T9, len1A_out_ga(T18, X27)) → len1B_out_ga(.(T6, .(T17, T18)), T9)
len1B_in_ga(.(T6, .(T17, T18)), s(s(T38))) → U4_ga(T6, T17, T18, T38, len1A_in_ga(T18, T38))
U4_ga(T6, T17, T18, T38, len1A_out_ga(T18, T38)) → len1B_out_ga(.(T6, .(T17, T18)), s(s(T38)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
len1B_in_ga([], 0) → len1B_out_ga([], 0)
len1B_in_ga(.(T6, []), s(0)) → len1B_out_ga(.(T6, []), s(0))
len1B_in_ga(.(T6, .(T17, T18)), T9) → U3_ga(T6, T17, T18, T9, len1A_in_ga(T18, X27))
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T24, T25), X42) → U1_ga(T24, T25, X42, len1A_in_ga(T25, X41))
len1A_in_ga(.(T24, T25), s(T29)) → U2_ga(T24, T25, T29, len1A_in_ga(T25, T29))
U2_ga(T24, T25, T29, len1A_out_ga(T25, T29)) → len1A_out_ga(.(T24, T25), s(T29))
U1_ga(T24, T25, X42, len1A_out_ga(T25, X41)) → len1A_out_ga(.(T24, T25), X42)
U3_ga(T6, T17, T18, T9, len1A_out_ga(T18, X27)) → len1B_out_ga(.(T6, .(T17, T18)), T9)
len1B_in_ga(.(T6, .(T17, T18)), s(s(T38))) → U4_ga(T6, T17, T18, T38, len1A_in_ga(T18, T38))
U4_ga(T6, T17, T18, T38, len1A_out_ga(T18, T38)) → len1B_out_ga(.(T6, .(T17, T18)), s(s(T38)))
LEN1B_IN_GA(.(T6, .(T17, T18)), T9) → U3_GA(T6, T17, T18, T9, len1A_in_ga(T18, X27))
LEN1B_IN_GA(.(T6, .(T17, T18)), T9) → LEN1A_IN_GA(T18, X27)
LEN1A_IN_GA(.(T24, T25), X42) → U1_GA(T24, T25, X42, len1A_in_ga(T25, X41))
LEN1A_IN_GA(.(T24, T25), X42) → LEN1A_IN_GA(T25, X41)
LEN1A_IN_GA(.(T24, T25), s(T29)) → U2_GA(T24, T25, T29, len1A_in_ga(T25, T29))
LEN1A_IN_GA(.(T24, T25), s(T29)) → LEN1A_IN_GA(T25, T29)
LEN1B_IN_GA(.(T6, .(T17, T18)), s(s(T38))) → U4_GA(T6, T17, T18, T38, len1A_in_ga(T18, T38))
LEN1B_IN_GA(.(T6, .(T17, T18)), s(s(T38))) → LEN1A_IN_GA(T18, T38)
len1B_in_ga([], 0) → len1B_out_ga([], 0)
len1B_in_ga(.(T6, []), s(0)) → len1B_out_ga(.(T6, []), s(0))
len1B_in_ga(.(T6, .(T17, T18)), T9) → U3_ga(T6, T17, T18, T9, len1A_in_ga(T18, X27))
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T24, T25), X42) → U1_ga(T24, T25, X42, len1A_in_ga(T25, X41))
len1A_in_ga(.(T24, T25), s(T29)) → U2_ga(T24, T25, T29, len1A_in_ga(T25, T29))
U2_ga(T24, T25, T29, len1A_out_ga(T25, T29)) → len1A_out_ga(.(T24, T25), s(T29))
U1_ga(T24, T25, X42, len1A_out_ga(T25, X41)) → len1A_out_ga(.(T24, T25), X42)
U3_ga(T6, T17, T18, T9, len1A_out_ga(T18, X27)) → len1B_out_ga(.(T6, .(T17, T18)), T9)
len1B_in_ga(.(T6, .(T17, T18)), s(s(T38))) → U4_ga(T6, T17, T18, T38, len1A_in_ga(T18, T38))
U4_ga(T6, T17, T18, T38, len1A_out_ga(T18, T38)) → len1B_out_ga(.(T6, .(T17, T18)), s(s(T38)))
LEN1B_IN_GA(.(T6, .(T17, T18)), T9) → U3_GA(T6, T17, T18, T9, len1A_in_ga(T18, X27))
LEN1B_IN_GA(.(T6, .(T17, T18)), T9) → LEN1A_IN_GA(T18, X27)
LEN1A_IN_GA(.(T24, T25), X42) → U1_GA(T24, T25, X42, len1A_in_ga(T25, X41))
LEN1A_IN_GA(.(T24, T25), X42) → LEN1A_IN_GA(T25, X41)
LEN1A_IN_GA(.(T24, T25), s(T29)) → U2_GA(T24, T25, T29, len1A_in_ga(T25, T29))
LEN1A_IN_GA(.(T24, T25), s(T29)) → LEN1A_IN_GA(T25, T29)
LEN1B_IN_GA(.(T6, .(T17, T18)), s(s(T38))) → U4_GA(T6, T17, T18, T38, len1A_in_ga(T18, T38))
LEN1B_IN_GA(.(T6, .(T17, T18)), s(s(T38))) → LEN1A_IN_GA(T18, T38)
len1B_in_ga([], 0) → len1B_out_ga([], 0)
len1B_in_ga(.(T6, []), s(0)) → len1B_out_ga(.(T6, []), s(0))
len1B_in_ga(.(T6, .(T17, T18)), T9) → U3_ga(T6, T17, T18, T9, len1A_in_ga(T18, X27))
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T24, T25), X42) → U1_ga(T24, T25, X42, len1A_in_ga(T25, X41))
len1A_in_ga(.(T24, T25), s(T29)) → U2_ga(T24, T25, T29, len1A_in_ga(T25, T29))
U2_ga(T24, T25, T29, len1A_out_ga(T25, T29)) → len1A_out_ga(.(T24, T25), s(T29))
U1_ga(T24, T25, X42, len1A_out_ga(T25, X41)) → len1A_out_ga(.(T24, T25), X42)
U3_ga(T6, T17, T18, T9, len1A_out_ga(T18, X27)) → len1B_out_ga(.(T6, .(T17, T18)), T9)
len1B_in_ga(.(T6, .(T17, T18)), s(s(T38))) → U4_ga(T6, T17, T18, T38, len1A_in_ga(T18, T38))
U4_ga(T6, T17, T18, T38, len1A_out_ga(T18, T38)) → len1B_out_ga(.(T6, .(T17, T18)), s(s(T38)))
LEN1A_IN_GA(.(T24, T25), s(T29)) → LEN1A_IN_GA(T25, T29)
LEN1A_IN_GA(.(T24, T25), X42) → LEN1A_IN_GA(T25, X41)
len1B_in_ga([], 0) → len1B_out_ga([], 0)
len1B_in_ga(.(T6, []), s(0)) → len1B_out_ga(.(T6, []), s(0))
len1B_in_ga(.(T6, .(T17, T18)), T9) → U3_ga(T6, T17, T18, T9, len1A_in_ga(T18, X27))
len1A_in_ga([], 0) → len1A_out_ga([], 0)
len1A_in_ga(.(T24, T25), X42) → U1_ga(T24, T25, X42, len1A_in_ga(T25, X41))
len1A_in_ga(.(T24, T25), s(T29)) → U2_ga(T24, T25, T29, len1A_in_ga(T25, T29))
U2_ga(T24, T25, T29, len1A_out_ga(T25, T29)) → len1A_out_ga(.(T24, T25), s(T29))
U1_ga(T24, T25, X42, len1A_out_ga(T25, X41)) → len1A_out_ga(.(T24, T25), X42)
U3_ga(T6, T17, T18, T9, len1A_out_ga(T18, X27)) → len1B_out_ga(.(T6, .(T17, T18)), T9)
len1B_in_ga(.(T6, .(T17, T18)), s(s(T38))) → U4_ga(T6, T17, T18, T38, len1A_in_ga(T18, T38))
U4_ga(T6, T17, T18, T38, len1A_out_ga(T18, T38)) → len1B_out_ga(.(T6, .(T17, T18)), s(s(T38)))
LEN1A_IN_GA(.(T24, T25), s(T29)) → LEN1A_IN_GA(T25, T29)
LEN1A_IN_GA(.(T24, T25), X42) → LEN1A_IN_GA(T25, X41)
LEN1A_IN_GA(.(T24, T25)) → LEN1A_IN_GA(T25)
From the DPs we obtained the following set of size-change graphs: